2020最具“战略性”的编程语言：C语言？还是C# 、 Python 、Swift？

编程语言是人们指导或控制机器的工具，其开发目的在于让操控机器的过程更加简单和顺畅。正因如此，数百种编程语言应运而生。然而，它们的命运却各不相同。一些语言已不复使用，或将在未来几年淘汰。相应地，一些语言将会被充分使用，还有一些崭新的编程语言正在逐渐被人们所接受。

“虽然程序漏洞的检测和验证已经引起业界的高度重视，但在区块链行业内，安全问题仍旧频繁发生。如果只检测已经存在的漏洞的话，永远存在被黑客抢先一步的风险。既然这样，我们有没有办法直接开发出一个没有程序漏洞的、可以完全被信赖的智能合约呢？”

CertiK联合创始人顾荣辉在开发者大会上提到了智能合约安全的源头问题。

DeepSEA项目为了攻克这些更加底层可能出现的问题与隐患而诞生。

前天发布的【宅在家里最适合看的编程，C++、Java还是……沈从文？】已经简单介绍了DeepSEA的基础概念，那么现在让我们来了解一下DeepSEA的运行机制和执行过程。

DeepSEA是一种灵活且兼容的语言，可以使用Coq创建具有高度抽象和推理功能的安全程序。它旨在提供使用Coq证明助手来进行形式化验证的智能合约功能属性的方法。

现如今许多关于智能合约验证的工作都是围绕自动证明（例如Z3）建立的。这种功能可以简单陈述一个定理，并尝试证明这一定理。对于以下相对简单的证明、算术表达式和数据结构（如数组），这种功能最为有用。在该定理自定义甚至陈述状态的情况下，自动工具往往会卡顿。Coq是一个交互式证明助手，它不会证明定理：用户必须同时编写定理陈述和证明，然后Coq会检查证明是否正确。这将涉及更多的工作，但它同时也可以处理任意高级数学问题。

为了推理出Coq中合约的正确性，需要定义一个正在执行的模型，该模型可以加载到Coq证明助手中。现在CertiK团队研发的方法是使用相当小的编程语言（DeepSEA语言）编写合约。DeepSEA编译器不仅将合约编译为EVM字节码，还输出可以加载的表示形式进入Coq。从而可以推断出合约的高级表示形式。由于技术人员还验证了DeepSEA编译器的正确性，所以可以确保生成的Coq合约表示形式与已编译的EVM字节码的工作相契合。

示例：使用Coq验证通证合约

DeepSEA语言受ML和Coq本身等功能语言的启发。下面的代码显示了通证合约的总体外观，以它为运行示例。

下图显示了将通证合约编译为EVM的过程。编译过程首先要解析合约并对其进行类型检查，然后生成一组相应的Coq文件。技术团队将这些文件与经过验证的编译器后端链接，然后使用Coq的提取工具将其编译为OCaml，从而生成EVM程序集。最后，打印机通道（未经验证，用OCaml编写）可以将程序集转换为实际的字节码。即可通过将合约部署到Ganache实例中并调用函数来演示合约的运行过程。

为了方便起见，CertiK开发了一个DeepSEA编译器，它被编译为单个OCaml可执行文件，用户无需在计算机上安装Coq即可运行它。这用（未经验证的）OCaml代码替换了用Coq编写的某些编译器，因此可信度较低，并且不会生成合约的Coq表示形式。下图显示的编译器正在运行，它能生成与上面Coq版本相同的字节码。我们还可以打印出中间语言表示形式或EVM汇编助记符。

现在我们可以将合约表示形式加载到Coq中，并开始编写有关它的证明。合约表示为用Coq的内置编程语言“ Gallina”编写的功能，如下所示。由于这是用户将在证明中使用的版本，因此我们希望它以清晰的方式与输入程序相对应并实现大部分的功能。这一点可以通过使用Gallina语言（不是DeepSEA语言）以及monadic组合器编写来实现。

如果我们查看细节，那么从某种角度来说，Coq表示实际上比输入程序更高级，更易于推理。虽然已编译的以太坊哈希值无法跟踪存储在程序中的密钥，但在Coq版本中，我们可以使用Int256Tree数据表示余额，该数据类型表会储存其密钥。尽管可执行程序使用的是256个整数，但表示形式可使用的整数是无限的，因此表示形式可以用普通算术实现。（下文将会讨论如何处理整数溢出。）

下图显示了使用Coq证明助手来证明合约的transfer方法保留了余额中存储的代币。换句话说，其中没有可以创建或销毁通证的漏洞。（有可能出问题的地方就是代码检查整数溢出，并检查发送和接收帐户是否不同的环节。如果忘记了其中一个if语句，则该定理将不可证明。） Coq是一个交互式操作：计算机不断显示要证明的内容，程序员输入一系列命令，将定理分解为更简单的语句。

除了最终合约之外，DeepSEA系统还生成了一组附带条件，必须证明这些附带条件对合约是有效的，且多数情况下不存在整数溢出。在Solidity语言中，程序员通常使用“安全机制”库，并在该库中添加证明语句，以在发生整数溢出时还原合约调用函数的过程。DeepSEA提供了插入语句，在这种情况下，附带条件显得微不足道。通过一些措施，目前可以证明transfer方法中的整数不会溢出。

证明（下图中的摘录）余额中存储值的不变性有关，所以实际上整个过程并不需要安全保证性语句。这是一个用程序验证如何提高效率的例子，它帮助程序员去使用更多编程技术，使它们可操作性和安全性都得到保证。

在接下来的几周和几个月中，CertiK将发布更多项目，例如下载编译器，语言手册草案，更多示例证明以及最终实现案例等。

DeepSEA正式上线，复制链接【https://certik.org/research/deepsea/】至浏览器即可查看DeepSEA上线产品。

了解更多

General Information: [e-mail]

Audit & Partnerships: [e-mail]

Website: certik.org

Twitter: @certik.org

Telegram: t.me/certik.org

Medium:medium.com/certik

币乎：bihu.com/people/1093109

往期回顾

请点击“阅读原文”访问CertiK官方网站